So...

As you will have seen in the university, you have the opportunity to throw in the event title for a course like this, which is so relevant and which refers to W3C standards and the like.

So essentially this is...

A course in Formal Knowledge Representation.

So after this word, I would like to go into the field of the professor of knowledge representation and processing. De facto, this is not quite the case and we were there first.

So it is a bit of a cross-cut with the actual areas of the professor. So it is nothing that is highly correlated. So we are doing formal knowledge representation, namely specific languages and algorithms.

So this is a course in Formal Knowledge Representation, which is to be seen in direct connection to Gleun.

Were everyone in Gleun?

Or sometimes there are people from outside...

David, shake your head.

You weren't in Gleun.

No, the gentleman in the middle. You didn't lie.

I don't even know what that is.

Ah, you don't even know what that is. Very good. So Gleun is the course in Formal Knowledge Representation.

So there will be statements, logic and first step. What is your own background now?

I have a bachelor's degree in mechatronics.

Bachelor's degree in mechatronics. Okay. So basically we are doing it without any conditions.

I will start a special lesson on logic and first step, which basically does everything from the beginning.

I would still recommend you to take a look at Gleun's script. It will help you.

Okay. What does Formal Knowledge Representation mean? Formal Knowledge Representation means that we try to formalize world knowledge in such a way that it can be processed by the computer.

So this is generally the overall melody of this not small area of knowledge representation and processing.

As I said, this is an area where there are conferences that are called that. This is represented at the big AI conferences.

There is a W3C standard for the Web Ontology Language.

Even if you don't know it that way, this is information mainstream.

We are hanging around different expression strengths through logic. We start with logic that we already know, from Gleun.

We will start with logic of first step. You might think, we know that from Gleun, but we don't need that.

There are many things about logic of first step that we don't know in Gleun.

We want to show the indecisiveness.

I can't build a perfect first order proof that tells me if it is valid or not.

We want to say things about the expression strength of logic of first step, especially methods to know how to limit this expression strength upwards.

Generally, you can see here, even in the negative, two main topics that jump against each other in knowledge representation.

What do you do in formal knowledge representation? You build formalisms in which you can write things that you want to be the most expression-strong.

That you can write as many things as possible.

But you have to balance that against another requirement. You want to process this knowledge in the computer, especially something like automatic closing.

The common ontology systems do that too. It is a big industry to build all-reasoners. There are companies that don't do anything but to tick all-reasoners.

The more expression-strong the language is, the more difficult it is to draw conclusions.

In formal language representation, this is a relatively strong expression-strong language.

Even if we want negative results, I can express a lot, but not everything.

Especially not everything I want to express. But because it is so expression-strong, it is indecisive.

In summary, first step in logic as knowledge representation is nothing that would not be used at all, but not the formalism that has finally been implemented.

Then we take a step back and do statement logic again.

The statement logic is now very expression-strong. We can only express very little in it. For that we already know from Gleun that statement logic is decidable.

The usual algorithm is the P against NP threshold. Makeable problems are in P and non-makeable problems are in NP.

In this sense, statement logic is a non-makeable problem. In statement logic, validity is in NP.

In the sense of logic, statement logic is ridiculous simple, in which validity is in NP.

I can actually write an NP algorithm that decides statement logic.

Not the obvious algorithm, I guess a truth condition and see if it does.

The logic itself moves to the top of NP. We will get to know a formalism that moves from the bottom of NP.

I will mention that in a moment. But if you show something like this in logic, he will doubt that this is still logic.

I talked to the late pope of intuitionist logic about EL. He said that this is not logic. This is something, but logic can not be called that anymore.